A, B:Realizer.
((Rplus?(A)))
 ((Rplus?(B)))
 ((Rnone?(A)))
 ((Rnone?(B)))
 (x:MaName. ((x  R-names(A)) & (x  R-names(B))))
 (R-loc(A) = R-loc(B)  Id)
 R-discrete_compat(A;B) 

latex

Definitions

tl(l), {T}, P  Q, i <z j, b, i z j, nth_tl(n;as), hd(l), A  B, i  j < k, Y, ||as||, {i..j}, l[i], A c B, MaName, False, Reffect-f(x1), Rinit-v(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), Reffect-x(x1), Reffect?(x1), , True, if b then t else f fi , tt, ff, x. t(x), t  T, R-discrete_compat(A;B), P & Q, Rnone?(x1), Rplus?(x1), b, A, P  Q, Realizer, x:A. B(x), Dec(P), P  Q, P  Q, x(s), Unit, R-loc(R), R-names(A), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),

Lemmas

non neg length, length wf1, decidable equal MaName, locknd wf, fpf-domain wf, map wf, cons member, member singleton, le wf, select member, LocKnd wf, Rnone? wf, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, R-names wf, l member wf, MaName wf, Rinit wf, R-loc wf, false wf, Rplus? wf, assert wf, true wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf